Nuprl Definition : existse-le
0,22
postcript
pdf
e
e'
.
P
(
e
) ==
e
:E.
e
e'
&
P
(
e
)
latex
clarification:
existse-le(
es
;
e'
;
e
.
P
(
e
)) ==
e
:es-E(
es
). es-le(
es
;
e
;
e'
) &
P
(
e
)
latex
Definitions
x
:
A
.
B
(
x
)
,
E
,
A
&
B
,
e
e'
FDL editor aliases
existse-le
origin
e
e'.P(e) == e:E. e e' & P(e)
e:es-E(es). es-le(es;e;e') & P(e) ee'.P(e) == e:E. e e' & P(e)
e:es-E(es). es-le(es;e;e') & P(e) x:A. B(x) e'